(declare-fun a () String)
(assert (= (str.replace_all (str.++ (str.replace_all (str.replace_all (str.replace_all (str.replace_all (str.++ a a) "-" (str.++ a a)) a (str.++ a a a)) "-" (str.++ a a)) a (str.replace_all (str.++ a a) "-" (str.replace_all (str.++ a a) "-" (str.++ a a)))) (str.replace_all (str.replace_all (str.replace_all (str.++ a a) a (str.++ a a)) "-" (str.++ a a)) "-" (str.replace_all (str.replace_all (str.++ a a) "-" (str.replace_all "-" a (str.++ a a))) "-" (str.replace_all (str.++ a a) "-" (str.replace_all (str.++ a a a) "-" (str.++ a a)))))) (ite (= "-" a) a "") (str.++ (str.replace_all (str.++ a a) a (str.++ a a)) (str.replace_all (str.replace_all (str.replace_all (str.++ a a) "-" (str.++ a a)) "-" (str.replace_all (str.++ a a) "-" (str.++ a a))) (str.replace_all (str.++ a a) "-" (str.replace (str.replace_all (str.++ a a) "-" (str.++ a a)) "-" "")) (str.replace_all (str.replace_all (str.++ a a a) "-" (str.++ a a a)) a (str.++ a a))))) a))
(check-sat)
